x, y:3. rps(x;y)  rps(y;x) 

latex

Definitions

P  Q, A, b, x:AB(x), {i..j}, x:A. B(x), t  T, #$n, ij, true, false, s ~ t, SQType(T), {T}, SqStable(P), rps(x;y), P  Q, if b t else f fi, Case b of inl(x)  s(x) ; inr(y)  t(y), if a=b c ; d fi, left+right, Unit, P  Q, x:AB(x), P  Q, T, a<b, s = t, b, i<j, True, Prop, Type, , , i  j < k, AB, P & Q, False, Void, p  q, p  q, i=j, {x:A| B(x) }

Lemmas

eq int wf, band wf, bor wf, assert wf, bool wf, le int wf, lt int wf, bnot wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, le wf, assert of le int, eqtt to assert, assert of bor, assert of eq int, assert of band, and functionality wrt iff, or functionality wrt iff, decidable lt, sq stable from decidable, decidable le, sq stable and, bfalse wf, btrue wf, int seg wf